﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

using Compiler.CompilerAPI;
using Compiler.TableOfSymbols.Types;
using Compiler.Unification.Constraints;
using Compiler.Unification.Substitutions;
using Compiler.Unification.Auxiliary;
using Compiler.TableOfSymbols.Concepts;

namespace Compiler.Unification
{
    /// <summary>
    /// Алгоритм унификации
    /// </summary>
    public class UnifyAlgo
    {
        private CompilationEnvironment environment;
        private AuxiliaryUnifyAlgos auxAlgos;

        private ConceptDefinition concept;

        private ConstraintsQueue constraints;
        private HashSet<BaseTypeConstraint> resultConstraints = null;
        private Substitution subs;

        private int typeVarCounter = 0;
        private string NextTypeVarName
        {
            get 
            { 
                ++typeVarCounter; 
                return "TV" + typeVarCounter.ToString(); 
            }
        }

        public ConceptDefinition Concept
        {
            get { return concept; }
        }

        public Substitution TypesSubstitution
        {
            get { return subs; }
        }

        public HashSet<BaseTypeConstraint> ResultConstraints
        {
            get 
            {
                if (resultConstraints != null)
                    return resultConstraints;
                else
                {
                    resultConstraints = new HashSet<BaseTypeConstraint>();
                    while (!constraints.IsEmpty)
                        resultConstraints.Add(constraints.Dequeue());
                    return resultConstraints;
                }
            }
        }

        public UnifyAlgo(CompilationEnvironment environment, ConceptDefinition concept, HashSet<BaseTypeConstraint> constraints)
        {
            if (environment == null)
                throw new ArgumentNullException("environment can not be null");
            if (constraints == null)
                throw new ArgumentNullException("constraints can not be null");
            if (concept == null)
                throw new ArgumentNullException("concept can not be null");
            this.environment = environment;
            this.concept = concept;
            this.constraints = new ConstraintsQueue(environment.TypesBijectiveMap, constraints);
            this.subs = new Substitution(environment.TypesBijectiveMap);
            this.auxAlgos = new AuxiliaryUnifyAlgos(environment, concept);
        }

        public bool Unify()
        {
            if (constraints.IsEmpty)
                return true;
            BaseTypeConstraint constraint = constraints.Peek();
            if (constraint.ViewCount == 1)
                return true;
            constraint = constraints.Dequeue();
            if (constraint.IsSameType)
                return ProcessSametypeConstraint(constraint as SametypeConstraint);
            else
                return ProcessSubtypingConstraint(constraint as SubtypingConstraint);
        }

        private bool ProcessSametypeConstraint(SametypeConstraint constraint)
        {
            System.Diagnostics.Debug.Assert(constraint != null,
                "SametypeConstraint myst be here");
            if (constraint.LeftTypeArgument == constraint.RightTypeArgument)
                return Unify();
            if (constraint.LeftTypeArgument.IsTypeValue)
                if (constraint.RightTypeArgument.IsTypeValue)
                    return _ProcessSametypeConstraintValVal(
                        constraint.LeftTypeArgument as TypeValue,
                        constraint.RightTypeArgument as TypeValue);
                else
                    return _ProcessSametypeConstraintVarVal(
                        constraint.RightTypeArgument as TypeVariable,
                        constraint.LeftTypeArgument as TypeValue);
            else
                if (constraint.RightTypeArgument.IsTypeValue)
                    return _ProcessSametypeConstraintVarVal(
                        constraint.LeftTypeArgument as TypeVariable,
                        constraint.RightTypeArgument as TypeValue);
                else
                    return _ProcessSametypeConstraintVarVar(
                        constraint.RightTypeArgument as TypeVariable,
                        constraint.LeftTypeArgument as TypeVariable);
        }

        private bool ProcessSubtypingConstraint(SubtypingConstraint constraint)
        {
            System.Diagnostics.Debug.Assert(constraint != null,
                "SubtypingConstraint myst be here");
            if (constraint.LeftTypeArgument == constraint.RightTypeArgument)
                return Unify();
            if (constraint.LeftTypeArgument.IsTypeValue)
                if (constraint.RightTypeArgument.IsTypeValue)
                    return _ProcessSubtypingConstraintValVal(
                        constraint.LeftTypeArgument as TypeValue,
                        constraint.RightTypeArgument as TypeValue);
                else
                    return _ProcessSubtypingConstraintValVar(
                        constraint.LeftTypeArgument as TypeValue,
                        constraint.RightTypeArgument as TypeVariable);
            else
                if (constraint.RightTypeArgument.IsTypeValue)
                    return _ProcessSubtypingConstraintVarVal(
                        constraint.LeftTypeArgument as TypeVariable,
                        constraint.RightTypeArgument as TypeValue);
                else
                    return _ProcessSubtypingConstraintVarVar(
                        constraint.LeftTypeArgument as TypeVariable,
                        constraint.RightTypeArgument as TypeVariable);
        }

        // -------------------------------------- Sametype constraint 

        private bool _ProcessSametypeConstraintValVal(TypeValue s, TypeValue t)
        {
            System.Diagnostics.Debug.Assert(s != t,
                "s and t must be already distinct here");
            bool constraintsAdded;
            bool result = auxAlgos.AreEqual(s, t, this.constraints, out constraintsAdded);
            if (result)
                return Unify();
            else
                return auxAlgos.AddEqualError(s, t);
        }

        private bool _ProcessSametypeConstraintVarVal(TypeVariable s, TypeValue t)
        {
            if (_TypeVarRecursivelyOccurres(s, t))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивная подстановка {1} вместо {0} недопустима",
                        environment.TypesBijectiveMap.GetTypeName(s), 
                        environment.TypesBijectiveMap.GetTypeName(t))));
                return false;
            }
            bool constraintsAdded;
            if (auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t, constraints, out constraintsAdded))
                if (auxAlgos.LeftIsSubtypeOrEqual(t, s.MinUpperType, constraints, out constraintsAdded))
                {
                    SubstitutionItem sub = new SubstitutionItem(s, t);
                    this.constraints.ApplySubstitutionItem(sub);
                    bool result = Unify();
                    this.subs.ComposeWith(sub);
                    return result;
                }
                else
                    return auxAlgos.AddSubtypingError(t, s.MinUpperType);
            else
                return auxAlgos.AddSubtypingError(s.MaxLowerType, t);
        }

        private bool _TypeVarRecursivelyOccurres(TypeVariable s, TypeValue t)
        {
            if (t.IsNETClassTypeValue && environment.TypesBijectiveMap[t].IsGenericType)
            {
                Type genTypeNET = environment.TypesBijectiveMap[t];
                IEnumerable<Type> allVarArgsNET = _GetGenericTypeVarArguments(genTypeNET);
                IEnumerable<BaseType> allVarArgs = allVarArgsNET.Select(
                    nt => environment.TypesBijectiveMap[nt]);
                return allVarArgs.Contains(s);
            }
            return false;
        }
        private IEnumerable<Type> _GetGenericTypeVarArguments(Type genTypeNET)
        {
            System.Diagnostics.Debug.Assert(genTypeNET.IsGenericType && !genTypeNET.IsGenericTypeDefinition,
                "genTypeNET must be generic type, not definition");
            IEnumerable<Type> args = genTypeNET.GenericTypeArguments;
            IEnumerable<Type> vars = args.Where(t => t.IsGenericParameter);
            IEnumerable<Type> genericArgs = args.Where(t => t.IsGenericType);
            foreach (Type genericArg in genericArgs)
                vars = vars.Union(_GetGenericTypeVarArguments(genericArg));
            return vars;
        }

        private bool _ProcessSametypeConstraintVarVar(TypeVariable s, TypeVariable t)
        {
            bool constraintsAdded;
            if (!(auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t.MinUpperType, constraints, out constraintsAdded)
                && auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t.MinUpperType, constraints, out constraintsAdded)))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                String.Format(auxAlgos.ConceptTitle + "Границы ({1}, {2}) типовой переменной {0} не совместимы с границами ({4}, {5}) типовой переменной {3}",
                    environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(s.MaxLowerType),
                    environment.TypesBijectiveMap.GetTypeName(s.MinUpperType), environment.TypesBijectiveMap.GetTypeName(t),
                    environment.TypesBijectiveMap.GetTypeName(t.MaxLowerType), environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                return false;
            }
            TypeValue lower, upper;
            if (auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t.MaxLowerType, constraints, out constraintsAdded))
                lower = t.MaxLowerType;
            else if (auxAlgos.LeftIsSubtypeOrEqual(t.MaxLowerType, s.MaxLowerType, constraints, out constraintsAdded))
                lower = s.MaxLowerType;
            else
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                String.Format(auxAlgos.ConceptTitle + "Нижняя граница {1} типовой переменной {0} не совместима с нижней границей {3} типовой переменной {2}",
                    environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(s.MaxLowerType),
                    environment.TypesBijectiveMap.GetTypeName(t), environment.TypesBijectiveMap.GetTypeName(t.MaxLowerType))));
                return false;
            }
            if (auxAlgos.LeftIsSubtypeOrEqual(s.MinUpperType, t.MinUpperType, constraints, out constraintsAdded))
                upper = s.MinUpperType;
            else if (auxAlgos.LeftIsSubtypeOrEqual(t.MinUpperType, s.MinUpperType, constraints, out constraintsAdded))
                upper = t.MinUpperType;
            else
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                String.Format(auxAlgos.ConceptTitle + "Верхняя граница {1} типовой переменной {0} не совместима с верхней границей {3} типовой переменной {2}",
                    environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(s.MinUpperType),
                    environment.TypesBijectiveMap.GetTypeName(t), environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                return false;
            }
            if (lower == upper)
            {
                SubstitutionItem subS = new SubstitutionItem(s, lower);
                SubstitutionItem subT = new SubstitutionItem(t, upper);
                this.constraints.ApplySubstitutionItem(subS);
                this.constraints.ApplySubstitutionItem(subT);
                bool result = Unify();
                this.subs.ComposeWith(subT);
                this.subs.ComposeWith(subS);
                return result;
            }
            else
            {
                Type newTypeVarNET = new NETTypeVariable(NextTypeVarName);
                environment.TypesBijectiveMap.AddPairByNETType(newTypeVarNET);
                BaseType newTypeVar = environment.TypesBijectiveMap[newTypeVarNET];
                SubstitutionItem subS = new SubstitutionItem(s, newTypeVar);
                SubstitutionItem subT = new SubstitutionItem(t, newTypeVar);
                this.constraints.ApplySubstitutionItem(subS);
                this.constraints.ApplySubstitutionItem(subT);
                bool result = Unify();
                this.subs.ComposeWith(subT);
                this.subs.ComposeWith(subS);
                return result;
            }
        }

        // -------------------------------------- Subtyping constraint 

        private bool _ProcessSubtypingConstraintValVal(TypeValue s, TypeValue t)
        {
            System.Diagnostics.Debug.Assert(s != t,
                "s and t must be already distinct here");
            bool constraintsAdded;
            if (auxAlgos.LeftIsSubtypeOrEqual(s, t, this.constraints, out constraintsAdded))
                return Unify();
            else
                return auxAlgos.AddSubtypingError(s, t); 
        }

        private bool _ProcessSubtypingConstraintValVar(TypeValue s, TypeVariable t)
        {
            System.Diagnostics.Debug.Assert(t != null,
                "t must be type variable here");
            if (_TypeVarRecursivelyOccurres(t, s))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивное ограниченние {0} <: {1} недопустимо",
                        environment.TypesBijectiveMap.GetTypeName(s),
                        environment.TypesBijectiveMap.GetTypeName(t))));
                return false;
            }
            bool constraintsAdded;
            if (s == t.MaxLowerType)
                return Unify();
            else if (auxAlgos.LeftIsSubtypeOrEqual(s, t.MaxLowerType, this.constraints, out constraintsAdded))
                return Unify();
            else if (auxAlgos.LeftIsSubtypeOrEqual(t.MaxLowerType, s, this.constraints, out constraintsAdded))
            {
                //if (s == t.MinUpperType)
                if (auxAlgos.AreEqual(s, t.MinUpperType, this.constraints, out constraintsAdded))
                {
                    SubstitutionItem subT = new SubstitutionItem(t, s);
                    this.constraints.ApplySubstitutionItem(subT);
                    bool result = Unify();
                    this.subs.ComposeWith(subT);
                    return result;
                }
                else if (auxAlgos.LeftIsSubtypeOrEqual(s, t.MinUpperType, this.constraints, out constraintsAdded))
                {
                    Type newTypeVarNET = new NETTypeVariable(NextTypeVarName);
                    TypeVariable newTypeVar = new TypeVariable(newTypeVarNET.Name, s, t.MinUpperType);
                    environment.TypesBijectiveMap.AddPair(newTypeVar, newTypeVarNET);
                    SubstitutionItem subT = new SubstitutionItem(t, newTypeVar);
                    this.constraints.ApplySubstitutionItem(subT);
                    bool result = Unify();
                    this.subs.ComposeWith(subT);
                    return result;
                }
                else if (auxAlgos.LeftIsSubtypeOrEqual(t.MinUpperType, s, this.constraints, out constraintsAdded))
                {
                    environment.ErrorManager.AddSemanticError(new UnificationError(
                        String.Format(auxAlgos.ConceptTitle + "Тип {0} не может быть подтипом типовой переменной {1}, так как является надтипом верхней границы {2}",
                            environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                            environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                    return false;
                }
                else
                    return auxAlgos.AddDifferentChainsError(s, t.MinUpperType);
            }
            else
                return auxAlgos.AddDifferentChainsError(s, t.MaxLowerType);
        }

        private bool _ProcessSubtypingConstraintVarVal(TypeVariable s, TypeValue t)
        {
            System.Diagnostics.Debug.Assert(s != null,
                "s must be type variable here");
            if (_TypeVarRecursivelyOccurres(s, t))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивное ограниченние {0} <: {1} недопустимо",
                        environment.TypesBijectiveMap.GetTypeName(s),
                        environment.TypesBijectiveMap.GetTypeName(t))));
                return false;
            }
            bool constraintsAdded;
            if (s.MinUpperType == t)
                return Unify();
            else if (auxAlgos.LeftIsSubtypeOrEqual(s.MinUpperType, t, this.constraints, out constraintsAdded))
                return Unify();
            else if (auxAlgos.LeftIsSubtypeOrEqual(t, s.MinUpperType, this.constraints, out constraintsAdded))
            {
                //if (t == s.MaxLowerType)
                if (auxAlgos.AreEqual(t, s.MaxLowerType, this.constraints, out constraintsAdded))
                {
                    SubstitutionItem subS = new SubstitutionItem(s, t);
                    this.constraints.ApplySubstitutionItem(subS);
                    bool result = Unify();
                    this.subs.ComposeWith(subS);
                    return result;
                }
                else if (auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t, this.constraints, out constraintsAdded))
                {
                    Type newTypeVarNET = new NETTypeVariable(NextTypeVarName);
                    TypeVariable newTypeVar = new TypeVariable(newTypeVarNET.Name, s.MaxLowerType, t);
                    environment.TypesBijectiveMap.AddPair(newTypeVar, newTypeVarNET);
                    SubstitutionItem subS = new SubstitutionItem(s, newTypeVar);
                    this.constraints.ApplySubstitutionItem(subS);
                    bool result = Unify();
                    this.subs.ComposeWith(subS);
                    return result;
                }
                else if (auxAlgos.LeftIsSubtypeOrEqual(t, s.MaxLowerType, this.constraints, out constraintsAdded))
                {
                    environment.ErrorManager.AddSemanticError(new UnificationError(
                        String.Format(auxAlgos.ConceptTitle + "Типовая переменная {0} не может быть подтипом {1}, так как он является подтипом её нижней границы {2}",
                            environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                            environment.TypesBijectiveMap.GetTypeName(s.MaxLowerType))));
                    return false;
                }
                else
                    return auxAlgos.AddDifferentChainsError(s.MaxLowerType, t);
            }
            else
                return auxAlgos.AddDifferentChainsError(s.MinUpperType, t);
        }

        private bool _ProcessSubtypingConstraintVarVar(TypeVariable s, TypeVariable t)
        {
            System.Diagnostics.Debug.Assert(s != null,
                "s must be type variable here");
            System.Diagnostics.Debug.Assert(t != null,
                "t must be type variable here");
            if (_TypeVarRecursivelyOccurres(s, t.MaxLowerType))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивное сравнение {0} и {1} недопустимо",
                        environment.TypesBijectiveMap.GetTypeName(s),
                        environment.TypesBijectiveMap.GetTypeName(t.MaxLowerType))));
                return false;
            }
            else if (_TypeVarRecursivelyOccurres(s, t.MinUpperType))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивное сравнение {0} и {1} недопустимо",
                        environment.TypesBijectiveMap.GetTypeName(s),
                        environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                return false;
            }
            else if (_TypeVarRecursivelyOccurres(t, s.MaxLowerType))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивное сравнение {0} и {1} недопустимо",
                        environment.TypesBijectiveMap.GetTypeName(s.MaxLowerType),
                        environment.TypesBijectiveMap.GetTypeName(t))));
                return false;
            }
            else if (_TypeVarRecursivelyOccurres(t, s.MinUpperType))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Рекурсивное сравнение {0} и {1} недопустимо",
                        environment.TypesBijectiveMap.GetTypeName(s.MinUpperType),
                        environment.TypesBijectiveMap.GetTypeName(t))));
                return false;
            }
            bool constraintsAdded;
            if (!auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t.MinUpperType, this.constraints, out constraintsAdded))
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Типовая переменная {0} не может быть подтипом типовой переменной {1},"
                        + "так как нижняя граница {2} первой переменной не является подтипом верхней границы {3} второй переменной",
                        environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                        environment.TypesBijectiveMap.GetTypeName(s.MaxLowerType), environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                return false;
            }
            if (auxAlgos.LeftIsSubtypeOrEqual(s.MaxLowerType, t.MaxLowerType, this.constraints, out constraintsAdded))
            {
                if (auxAlgos.LeftIsSubtypeOrEqual(s.MinUpperType, t.MaxLowerType, this.constraints, out constraintsAdded))
                    // ограничение остаётся
                    return _RecoverSubtypingConstraintWithViewCount(s, t, out constraintsAdded);
                else if (auxAlgos.LeftIsSubtypeOrEqual(t.MaxLowerType, s.MinUpperType, this.constraints, out constraintsAdded))
                {
                    if (auxAlgos.LeftIsSubtypeOrEqual(s.MinUpperType, t.MinUpperType, this.constraints, out constraintsAdded))
                        return _RecoverSubtypingConstraintWithViewCount(s, t, out constraintsAdded);
                    else if (auxAlgos.LeftIsSubtypeOrEqual(t.MinUpperType, s.MinUpperType, this.constraints, out constraintsAdded))
                    {
                        Type newTypeVarNET = new NETTypeVariable(NextTypeVarName);
                        TypeVariable newTypeVar = new TypeVariable(newTypeVarNET.Name, s.MaxLowerType, t.MinUpperType);
                        environment.TypesBijectiveMap.AddPair(newTypeVar, newTypeVarNET);
                        this.constraints.Enqueue(new SubtypingConstraint(newTypeVar, t));
                        constraintsAdded = true;
                        SubstitutionItem subS = new SubstitutionItem(s, newTypeVar);
                        this.constraints.ApplySubstitutionItem(subS);
                        bool result = Unify();
                        this.subs.ComposeWith(subS);
                        return result;
                    }
                    else
                    {
                        environment.ErrorManager.AddSemanticError(new UnificationError(
                            String.Format(auxAlgos.ConceptTitle + "Типовая переменная {0} не может быть подтипом типовой переменной {1},"
                                + "так как их верхние границы {2} и {3} находятся в разных цепочках наследования.",
                                environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                                environment.TypesBijectiveMap.GetTypeName(s.MinUpperType), environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                        return false;
                    }
                }
                else 
                {
                    environment.ErrorManager.AddSemanticError(new UnificationError(
                                String.Format(auxAlgos.ConceptTitle + "Типовая переменная {0} не может быть подтипом типовой переменной {1},"
                                    + "так как верхняя граница {2} первой переменной и нижняя {3} второй находятся в разных цепочках наследования.",
                                    environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                                    environment.TypesBijectiveMap.GetTypeName(s.MinUpperType), environment.TypesBijectiveMap.GetTypeName(t.MaxLowerType))));
                    return false;
                }
            }
            else if (auxAlgos.LeftIsSubtypeOrEqual(t.MaxLowerType, s.MaxLowerType, this.constraints, out constraintsAdded))
            {
                if (auxAlgos.LeftIsSubtypeOrEqual(t.MinUpperType, s.MinUpperType, this.constraints, out constraintsAdded))
                {
                    Type newTypeVarNETS = new NETTypeVariable(NextTypeVarName);
                    Type newTypeVarNETT = new NETTypeVariable(NextTypeVarName);
                    TypeVariable newTypeVarS = new TypeVariable(newTypeVarNETS.Name, s.MaxLowerType, t.MinUpperType);
                    TypeVariable newTypeVarT = new TypeVariable(newTypeVarNETT.Name, s.MaxLowerType, t.MinUpperType);
                    environment.TypesBijectiveMap.AddPair(newTypeVarS, newTypeVarNETS);
                    environment.TypesBijectiveMap.AddPair(newTypeVarT, newTypeVarNETT);
                    this.constraints.Enqueue(new SubtypingConstraint(newTypeVarS, newTypeVarT));
                    constraintsAdded = true;
                    SubstitutionItem subS = new SubstitutionItem(s, newTypeVarS);
                    SubstitutionItem subT = new SubstitutionItem(t, newTypeVarT);
                    this.constraints.ApplySubstitutionItem(subS);
                    this.constraints.ApplySubstitutionItem(subT);
                    bool result = Unify();
                    this.subs.ComposeWith(subT);
                    this.subs.ComposeWith(subS);
                    return result;
                }
                else if (auxAlgos.LeftIsSubtypeOrEqual(s.MinUpperType, t.MinUpperType, this.constraints, out constraintsAdded))
                {
                    Type newTypeVarNET = new NETTypeVariable(NextTypeVarName);
                    TypeVariable newTypeVar = new TypeVariable(newTypeVarNET.Name, s.MaxLowerType, t.MinUpperType);
                    environment.TypesBijectiveMap.AddPair(newTypeVar, newTypeVarNET);
                    this.constraints.Enqueue(new SubtypingConstraint(s, newTypeVar));
                    constraintsAdded = true;
                    SubstitutionItem subT = new SubstitutionItem(t, newTypeVar);
                    this.constraints.ApplySubstitutionItem(subT);
                    bool result = Unify();
                    this.subs.ComposeWith(subT);
                    return result;
                }
                else
                {
                    environment.ErrorManager.AddSemanticError(new UnificationError(
                                String.Format(auxAlgos.ConceptTitle + "Типовая переменная {0} не может быть подтипом типовой переменной {1},"
                                    + "так как их верхние границы {2} и {3} находятся в разных цепочках наследования.",
                                    environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                                    environment.TypesBijectiveMap.GetTypeName(s.MinUpperType), environment.TypesBijectiveMap.GetTypeName(t.MinUpperType))));
                    return false;
                }
            }
            else
            {
                environment.ErrorManager.AddSemanticError(new UnificationError(
                    String.Format(auxAlgos.ConceptTitle + "Типовая переменная {0} не может быть подтипом типовой переменной {1},"
                        + "так как их нижние границы {2} и {3} находятся в разных цепочках наследования.",
                        environment.TypesBijectiveMap.GetTypeName(s), environment.TypesBijectiveMap.GetTypeName(t),
                        environment.TypesBijectiveMap.GetTypeName(s.MaxLowerType), environment.TypesBijectiveMap.GetTypeName(t.MaxLowerType))));
                return false;
            }
        }

        private bool _RecoverSubtypingConstraintWithViewCount(TypeVariable s, TypeVariable t, out bool constraintsAdded)
        {
            constraints.Enqueue(new SubtypingConstraint(s, t, 1));
            constraintsAdded = true;
            return Unify();
        }
    }
}
